Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
snd: {1}
splitAt: {1, 2}
U21: {1}
U22: {1}
U31: {1}
U32: {1}
U41: {1}
U42: {1}
head: {1}
afterNth: {1, 2}
U51: {1}
U52: {1}
U61: {1}
U62: {1}
U63: {1}
U64: {1}
pair: {1, 2}
cons: {1}
U71: {1}
U72: {1}
U81: {1}
U82: {1}
fst: {1}
natsFrom: {1}
s: {1}
sel: {1, 2}
0: empty set
nil: empty set
tail: {1}
take: {1, 2}


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
snd: {1}
splitAt: {1, 2}
U21: {1}
U22: {1}
U31: {1}
U32: {1}
U41: {1}
U42: {1}
head: {1}
afterNth: {1, 2}
U51: {1}
U52: {1}
U61: {1}
U62: {1}
U63: {1}
U64: {1}
pair: {1, 2}
cons: {1}
U71: {1}
U72: {1}
U81: {1}
U82: {1}
fst: {1}
natsFrom: {1}
s: {1}
sel: {1, 2}
0: empty set
nil: empty set
tail: {1}
take: {1, 2}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
snd: {1}
splitAt: {1, 2}
U21: {1}
U22: {1}
U31: {1}
U32: {1}
U41: {1}
U42: {1}
head: {1}
afterNth: {1, 2}
U51: {1}
U52: {1}
U61: {1}
U62: {1}
U63: {1}
U64: {1}
pair: {1, 2}
cons: {1}
U71: {1}
U72: {1}
U81: {1}
U82: {1}
fst: {1}
natsFrom: {1}
s: {1}
sel: {1, 2}
0: empty set
nil: empty set
tail: {1}
take: {1, 2}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {snd, splitAt, head, afterNth, pair, fst, natsFrom, s, sel, tail, take, SND, SPLITAT, HEAD, AFTERNTH, FST, SEL, TAIL, TAKE, NATSFROM} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, cons, U71, U72, U81, U82, U121, U111, U221, U211, U321, U311, U421, U411, U521, U511, U621, U611, U631, U641, U721, U711, U821, U811} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U111(tt, N, XS) → U121(tt, N, XS)
U121(tt, N, XS) → SND(splitAt(N, XS))
U121(tt, N, XS) → SPLITAT(N, XS)
U211(tt, X) → U221(tt, X)
U311(tt, N) → U321(tt, N)
U411(tt, N, XS) → U421(tt, N, XS)
U421(tt, N, XS) → HEAD(afterNth(N, XS))
U421(tt, N, XS) → AFTERNTH(N, XS)
U511(tt, Y) → U521(tt, Y)
U611(tt, N, X, XS) → U621(tt, N, X, XS)
U621(tt, N, X, XS) → U631(tt, N, X, XS)
U631(tt, N, X, XS) → U641(splitAt(N, XS), X)
U631(tt, N, X, XS) → SPLITAT(N, XS)
U711(tt, XS) → U721(tt, XS)
U811(tt, N, XS) → U821(tt, N, XS)
U821(tt, N, XS) → FST(splitAt(N, XS))
U821(tt, N, XS) → SPLITAT(N, XS)
AFTERNTH(N, XS) → U111(tt, N, XS)
FST(pair(X, Y)) → U211(tt, X)
HEAD(cons(N, XS)) → U311(tt, N)
SEL(N, XS) → U411(tt, N, XS)
SND(pair(X, Y)) → U511(tt, Y)
SPLITAT(s(N), cons(X, XS)) → U611(tt, N, X, XS)
TAIL(cons(N, XS)) → U711(tt, XS)
TAKE(N, XS) → U811(tt, N, XS)

The collapsing dependency pairs are DPc:

U121(tt, N, XS) → N
U121(tt, N, XS) → XS
U221(tt, X) → X
U321(tt, N) → N
U421(tt, N, XS) → N
U421(tt, N, XS) → XS
U521(tt, Y) → Y
U631(tt, N, X, XS) → N
U631(tt, N, X, XS) → XS
U641(pair(YS, ZS), X) → X
U721(tt, XS) → XS
U821(tt, N, XS) → N
U821(tt, N, XS) → XS


The hidden terms of R are:

natsFrom(s(N))

Every hiding context is built from:

s on positions {1}
natsFrom on positions {1}

Hence, the new unhiding pairs DPu are :

U121(tt, N, XS) → U(N)
U121(tt, N, XS) → U(XS)
U221(tt, X) → U(X)
U321(tt, N) → U(N)
U421(tt, N, XS) → U(N)
U421(tt, N, XS) → U(XS)
U521(tt, Y) → U(Y)
U631(tt, N, X, XS) → U(N)
U631(tt, N, X, XS) → U(XS)
U641(pair(YS, ZS), X) → U(X)
U721(tt, XS) → U(XS)
U821(tt, N, XS) → U(N)
U821(tt, N, XS) → U(XS)
U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
U(natsFrom(s(N))) → NATSFROM(s(N))

The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The set Q consists of the following terms:

U11(tt, x0, x1)
U12(tt, x0, x1)
U21(tt, x0)
U22(tt, x0)
U31(tt, x0)
U32(tt, x0)
U41(tt, x0, x1)
U42(tt, x0, x1)
U51(tt, x0)
U52(tt, x0)
U61(tt, x0, x1, x2)
U62(tt, x0, x1, x2)
U63(tt, x0, x1, x2)
U64(pair(x0, x1), x2)
U71(tt, x0)
U72(tt, x0)
U81(tt, x0, x1)
U82(tt, x0, x1)
afterNth(x0, x1)
fst(pair(x0, x1))
head(cons(x0, x1))
natsFrom(x0)
sel(x0, x1)
snd(pair(x0, x1))
splitAt(0, x0)
splitAt(s(x0), cons(x1, x2))
tail(cons(x0, x1))
take(x0, x1)


The approximation of the Context-Sensitive Dependency Graph contains 2 SCCs with 35 less nodes.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
                ↳ QCSDPSubtermProof
              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {snd, splitAt, head, afterNth, pair, fst, natsFrom, s, sel, tail, take} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, cons, U71, U72, U81, U82} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)

The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The set Q consists of the following terms:

U11(tt, x0, x1)
U12(tt, x0, x1)
U21(tt, x0)
U22(tt, x0)
U31(tt, x0)
U32(tt, x0)
U41(tt, x0, x1)
U42(tt, x0, x1)
U51(tt, x0)
U52(tt, x0)
U61(tt, x0, x1, x2)
U62(tt, x0, x1, x2)
U63(tt, x0, x1, x2)
U64(pair(x0, x1), x2)
U71(tt, x0)
U72(tt, x0)
U81(tt, x0, x1)
U82(tt, x0, x1)
afterNth(x0, x1)
fst(pair(x0, x1))
head(cons(x0, x1))
natsFrom(x0)
sel(x0, x1)
snd(pair(x0, x1))
splitAt(0, x0)
splitAt(s(x0), cons(x1, x2))
tail(cons(x0, x1))
take(x0, x1)


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
                ↳ QCSDPSubtermProof
                  ↳ QCSDP
                    ↳ PIsEmptyProof
              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {snd, splitAt, head, afterNth, pair, fst, natsFrom, s, sel, tail, take} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, cons, U71, U72, U81, U82} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The set Q consists of the following terms:

U11(tt, x0, x1)
U12(tt, x0, x1)
U21(tt, x0)
U22(tt, x0)
U31(tt, x0)
U32(tt, x0)
U41(tt, x0, x1)
U42(tt, x0, x1)
U51(tt, x0)
U52(tt, x0)
U61(tt, x0, x1, x2)
U62(tt, x0, x1, x2)
U63(tt, x0, x1, x2)
U64(pair(x0, x1), x2)
U71(tt, x0)
U72(tt, x0)
U81(tt, x0, x1)
U82(tt, x0, x1)
afterNth(x0, x1)
fst(pair(x0, x1))
head(cons(x0, x1))
natsFrom(x0)
sel(x0, x1)
snd(pair(x0, x1))
splitAt(0, x0)
splitAt(s(x0), cons(x1, x2))
tail(cons(x0, x1))
take(x0, x1)


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
              ↳ QCSDP
                ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {snd, splitAt, head, afterNth, pair, fst, natsFrom, s, sel, tail, take, SPLITAT} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, cons, U71, U72, U81, U82, U621, U611, U631} we have µ(f) = {1}.

The TRS P consists of the following rules:

U611(tt, N, X, XS) → U621(tt, N, X, XS)
U621(tt, N, X, XS) → U631(tt, N, X, XS)
U631(tt, N, X, XS) → SPLITAT(N, XS)
SPLITAT(s(N), cons(X, XS)) → U611(tt, N, X, XS)

The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The set Q consists of the following terms:

U11(tt, x0, x1)
U12(tt, x0, x1)
U21(tt, x0)
U22(tt, x0)
U31(tt, x0)
U32(tt, x0)
U41(tt, x0, x1)
U42(tt, x0, x1)
U51(tt, x0)
U52(tt, x0)
U61(tt, x0, x1, x2)
U62(tt, x0, x1, x2)
U63(tt, x0, x1, x2)
U64(pair(x0, x1), x2)
U71(tt, x0)
U72(tt, x0)
U81(tt, x0, x1)
U82(tt, x0, x1)
afterNth(x0, x1)
fst(pair(x0, x1))
head(cons(x0, x1))
natsFrom(x0)
sel(x0, x1)
snd(pair(x0, x1))
splitAt(0, x0)
splitAt(s(x0), cons(x1, x2))
tail(cons(x0, x1))
take(x0, x1)


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


SPLITAT(s(N), cons(X, XS)) → U611(tt, N, X, XS)
The remaining pairs can at least be oriented weakly.

U611(tt, N, X, XS) → U621(tt, N, X, XS)
U621(tt, N, X, XS) → U631(tt, N, X, XS)
U631(tt, N, X, XS) → SPLITAT(N, XS)
Used ordering: Combined order from the following AFS and order.
U621(x1, x2, x3, x4)  =  x2
U611(x1, x2, x3, x4)  =  x2
U631(x1, x2, x3, x4)  =  x2
SPLITAT(x1, x2)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ AND
              ↳ QCSDP
              ↳ QCSDP
                ↳ QCSDPSubtermProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {snd, splitAt, head, afterNth, pair, fst, natsFrom, s, sel, tail, take, SPLITAT} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, cons, U71, U72, U81, U82, U621, U611, U631} we have µ(f) = {1}.

The TRS P consists of the following rules:

U611(tt, N, X, XS) → U621(tt, N, X, XS)
U621(tt, N, X, XS) → U631(tt, N, X, XS)
U631(tt, N, X, XS) → SPLITAT(N, XS)

The TRS R consists of the following rules:

U11(tt, N, XS) → U12(tt, N, XS)
U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)
U22(tt, X) → X
U31(tt, N) → U32(tt, N)
U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)
U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)
U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)
U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)
U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)
U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)
U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)
take(N, XS) → U81(tt, N, XS)

The set Q consists of the following terms:

U11(tt, x0, x1)
U12(tt, x0, x1)
U21(tt, x0)
U22(tt, x0)
U31(tt, x0)
U32(tt, x0)
U41(tt, x0, x1)
U42(tt, x0, x1)
U51(tt, x0)
U52(tt, x0)
U61(tt, x0, x1, x2)
U62(tt, x0, x1, x2)
U63(tt, x0, x1, x2)
U64(pair(x0, x1), x2)
U71(tt, x0)
U72(tt, x0)
U81(tt, x0, x1)
U82(tt, x0, x1)
afterNth(x0, x1)
fst(pair(x0, x1))
head(cons(x0, x1))
natsFrom(x0)
sel(x0, x1)
snd(pair(x0, x1))
splitAt(0, x0)
splitAt(s(x0), cons(x1, x2))
tail(cons(x0, x1))
take(x0, x1)


The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.